p2(a1(x0), p2(x1, p2(x2, x3))) -> p2(x1, p2(x0, p2(a1(x3), x3)))
↳ QTRS
↳ DependencyPairsProof
p2(a1(x0), p2(x1, p2(x2, x3))) -> p2(x1, p2(x0, p2(a1(x3), x3)))
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(a1(x3), x3)
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(x0, p2(a1(x3), x3))
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(x1, p2(x0, p2(a1(x3), x3)))
p2(a1(x0), p2(x1, p2(x2, x3))) -> p2(x1, p2(x0, p2(a1(x3), x3)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(a1(x3), x3)
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(x0, p2(a1(x3), x3))
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(x1, p2(x0, p2(a1(x3), x3)))
p2(a1(x0), p2(x1, p2(x2, x3))) -> p2(x1, p2(x0, p2(a1(x3), x3)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(a1(x3), x3)
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(x0, p2(a1(x3), x3))
Used ordering: Polynomial interpretation [21]:
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(x1, p2(x0, p2(a1(x3), x3)))
POL(P2(x1, x2)) = 2·x2
POL(a1(x1)) = 0
POL(p2(x1, x2)) = 1 + x2
p2(a1(x0), p2(x1, p2(x2, x3))) -> p2(x1, p2(x0, p2(a1(x3), x3)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
P2(a1(x0), p2(x1, p2(x2, x3))) -> P2(x1, p2(x0, p2(a1(x3), x3)))
p2(a1(x0), p2(x1, p2(x2, x3))) -> p2(x1, p2(x0, p2(a1(x3), x3)))